Theorem repizf 3864

Description: Axiom of Replacement. Axiom 7' of [Crosilla], p. "Axioms of CZF and IZF" (with unnecessary quantifier removed). In our context this is not an axiom, but a theorem proved from ax-coll 3863. It is identical to zfrep6 3865 except for the choice of a freeness hypothesis rather than a distinct variable constraint between 𝑏 and φ. (Contributed by Jim Kingdon, 23-Aug-2018.)

Hypothesis

Ref	Expression
ax-coll.1	⊢ Ⅎ𝑏φ

Assertion

Ref	Expression
repizf	⊢ (∀x ∈ 𝑎 ∃!yφ → ∃𝑏∀x ∈ 𝑎 ∃y ∈ 𝑏 φ)

Distinct variable group:   x,y,𝑎,𝑏

Allowed substitution hints:   φ(x,y,𝑎,𝑏)

Proof of Theorem repizf

Step	Hyp	Ref	Expression
1		euex 1927	. . 3 ⊢ (∃!yφ → ∃yφ)
2	1	ralimi 2378	. 2 ⊢ (∀x ∈ 𝑎 ∃!yφ → ∀x ∈ 𝑎 ∃yφ)
3		ax-coll.1	. . 3 ⊢ Ⅎ𝑏φ
4	3	ax-coll 3863	. 2 ⊢ (∀x ∈ 𝑎 ∃yφ → ∃𝑏∀x ∈ 𝑎 ∃y ∈ 𝑏 φ)
5	2, 4	syl 14	1 ⊢ (∀x ∈ 𝑎 ∃!yφ → ∃𝑏∀x ∈ 𝑎 ∃y ∈ 𝑏 φ)

Syntax hints:   → wi 4  Ⅎwnf 1346  ∃wex 1378  ∃!weu 1897  ∀wral 2300  ∃wrex 2301

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-coll 3863

This theorem depends on definitions:  df-bi 110  df-nf 1347  df-sb 1643  df-eu 1900  df-ral 2305

This theorem is referenced by:  zfrep6  3865  repizf2  3906