Theorem rexxfr3dALT

Description: Longer proof of rexxfr3d using ax-11 instead of ax-12 , without the disjoint variable condition A x y . (Contributed by SN, 19-Jun-2025) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rexxfr3dALT.s	⊢ ( 𝑥 = 𝑋 → ( 𝜓 ↔ 𝜒 ) )
	rexxfr3dALT.x	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ ∃ 𝑦 ∈ 𝐵 𝑥 = 𝑋 ) )
	rexxfr3dALT.a	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	rexxfr3dALT	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 ↔ ∃ 𝑦 ∈ 𝐵 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		rexxfr3dALT.s	⊢ ( 𝑥 = 𝑋 → ( 𝜓 ↔ 𝜒 ) )
2		rexxfr3dALT.x	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ ∃ 𝑦 ∈ 𝐵 𝑥 = 𝑋 ) )
3		rexxfr3dALT.a	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
4	2	anbi1d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ( ∃ 𝑦 ∈ 𝐵 𝑥 = 𝑋 ∧ 𝜓 ) ) )
5	1	pm5.32i	⊢ ( ( 𝑥 = 𝑋 ∧ 𝜓 ) ↔ ( 𝑥 = 𝑋 ∧ 𝜒 ) )
6	5	rexbii	⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝑥 = 𝑋 ∧ 𝜓 ) ↔ ∃ 𝑦 ∈ 𝐵 ( 𝑥 = 𝑋 ∧ 𝜒 ) )
7		r19.41v	⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝑥 = 𝑋 ∧ 𝜓 ) ↔ ( ∃ 𝑦 ∈ 𝐵 𝑥 = 𝑋 ∧ 𝜓 ) )
8	6 7	bitr3i	⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝑥 = 𝑋 ∧ 𝜒 ) ↔ ( ∃ 𝑦 ∈ 𝐵 𝑥 = 𝑋 ∧ 𝜓 ) )
9	4 8	bitr4di	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ∃ 𝑦 ∈ 𝐵 ( 𝑥 = 𝑋 ∧ 𝜒 ) ) )
10	9	exbidv	⊢ ( 𝜑 → ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ↔ ∃ 𝑥 ∃ 𝑦 ∈ 𝐵 ( 𝑥 = 𝑋 ∧ 𝜒 ) ) )
11		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜓 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) )
12		19.41v	⊢ ( ∃ 𝑥 ( 𝑥 = 𝑋 ∧ 𝜒 ) ↔ ( ∃ 𝑥 𝑥 = 𝑋 ∧ 𝜒 ) )
13	12	rexbii	⊢ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ( 𝑥 = 𝑋 ∧ 𝜒 ) ↔ ∃ 𝑦 ∈ 𝐵 ( ∃ 𝑥 𝑥 = 𝑋 ∧ 𝜒 ) )
14		rexcom4	⊢ ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ( 𝑥 = 𝑋 ∧ 𝜒 ) ↔ ∃ 𝑥 ∃ 𝑦 ∈ 𝐵 ( 𝑥 = 𝑋 ∧ 𝜒 ) )
15	13 14	bitr3i	⊢ ( ∃ 𝑦 ∈ 𝐵 ( ∃ 𝑥 𝑥 = 𝑋 ∧ 𝜒 ) ↔ ∃ 𝑥 ∃ 𝑦 ∈ 𝐵 ( 𝑥 = 𝑋 ∧ 𝜒 ) )
16	10 11 15	3bitr4g	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 ↔ ∃ 𝑦 ∈ 𝐵 ( ∃ 𝑥 𝑥 = 𝑋 ∧ 𝜒 ) ) )
17		elisset	⊢ ( 𝑋 ∈ 𝑉 → ∃ 𝑥 𝑥 = 𝑋 )
18	3 17	syl	⊢ ( 𝜑 → ∃ 𝑥 𝑥 = 𝑋 )
19	18	biantrurd	⊢ ( 𝜑 → ( 𝜒 ↔ ( ∃ 𝑥 𝑥 = 𝑋 ∧ 𝜒 ) ) )
20	19	rexbidv	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝐵 𝜒 ↔ ∃ 𝑦 ∈ 𝐵 ( ∃ 𝑥 𝑥 = 𝑋 ∧ 𝜒 ) ) )
21	16 20	bitr4d	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 ↔ ∃ 𝑦 ∈ 𝐵 𝜒 ) )