Metamath Proof Explorer


Theorem axrep4v

Description: Version of axrep4 with a disjoint variable condition, requiring fewer axioms. (Contributed by Matthew House, 18-Sep-2025)

Ref Expression
Assertion axrep4v ( ∀ 𝑥𝑧𝑦 ( 𝜑𝑦 = 𝑧 ) → ∃ 𝑧𝑦 ( 𝑦𝑧 ↔ ∃ 𝑥 ( 𝑥𝑤𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 ax-rep ( ∀ 𝑥𝑧𝑦 ( ∀ 𝑧 𝜑𝑦 = 𝑧 ) → ∃ 𝑧𝑦 ( 𝑦𝑧 ↔ ∃ 𝑥 ( 𝑥𝑤 ∧ ∀ 𝑧 𝜑 ) ) )
2 19.3v ( ∀ 𝑧 𝜑𝜑 )
3 2 imbi1i ( ( ∀ 𝑧 𝜑𝑦 = 𝑧 ) ↔ ( 𝜑𝑦 = 𝑧 ) )
4 3 albii ( ∀ 𝑦 ( ∀ 𝑧 𝜑𝑦 = 𝑧 ) ↔ ∀ 𝑦 ( 𝜑𝑦 = 𝑧 ) )
5 4 exbii ( ∃ 𝑧𝑦 ( ∀ 𝑧 𝜑𝑦 = 𝑧 ) ↔ ∃ 𝑧𝑦 ( 𝜑𝑦 = 𝑧 ) )
6 5 albii ( ∀ 𝑥𝑧𝑦 ( ∀ 𝑧 𝜑𝑦 = 𝑧 ) ↔ ∀ 𝑥𝑧𝑦 ( 𝜑𝑦 = 𝑧 ) )
7 2 anbi2i ( ( 𝑥𝑤 ∧ ∀ 𝑧 𝜑 ) ↔ ( 𝑥𝑤𝜑 ) )
8 7 exbii ( ∃ 𝑥 ( 𝑥𝑤 ∧ ∀ 𝑧 𝜑 ) ↔ ∃ 𝑥 ( 𝑥𝑤𝜑 ) )
9 8 bibi2i ( ( 𝑦𝑧 ↔ ∃ 𝑥 ( 𝑥𝑤 ∧ ∀ 𝑧 𝜑 ) ) ↔ ( 𝑦𝑧 ↔ ∃ 𝑥 ( 𝑥𝑤𝜑 ) ) )
10 9 albii ( ∀ 𝑦 ( 𝑦𝑧 ↔ ∃ 𝑥 ( 𝑥𝑤 ∧ ∀ 𝑧 𝜑 ) ) ↔ ∀ 𝑦 ( 𝑦𝑧 ↔ ∃ 𝑥 ( 𝑥𝑤𝜑 ) ) )
11 10 exbii ( ∃ 𝑧𝑦 ( 𝑦𝑧 ↔ ∃ 𝑥 ( 𝑥𝑤 ∧ ∀ 𝑧 𝜑 ) ) ↔ ∃ 𝑧𝑦 ( 𝑦𝑧 ↔ ∃ 𝑥 ( 𝑥𝑤𝜑 ) ) )
12 1 6 11 3imtr3i ( ∀ 𝑥𝑧𝑦 ( 𝜑𝑦 = 𝑧 ) → ∃ 𝑧𝑦 ( 𝑦𝑧 ↔ ∃ 𝑥 ( 𝑥𝑤𝜑 ) ) )