Theorem cbvex4v 979

Description: Rule used to change bound variables with implicit substitution.

Hypotheses

Ref	Expression
cbvex4v.1	⊢ ((x = v ∧ y = u) → (φ ↔ ψ))
cbvex4v.2	⊢ ((z = f ∧ w = g) → (ψ ↔ χ))

Assertion

Ref	Expression
cbvex4v	⊢ (∃x∃y∃z∃wφ ↔ ∃v∃u∃f∃gχ)

Distinct variable group(s):   v,u,φ   f,g,φ   x,y,χ   z,w,χ   ψ,x,y   ψ,f,g   x,z,w,u   y,z,w,v   z,g   w,f

Proof of Theorem cbvex4v

Step	Hyp	Ref	Expression
1		cbvex4v.1	. . . 4 ⊢ ((x = v ∧ y = u) → (φ ↔ ψ))
2	1	bi2exdv 938	. . 3 ⊢ ((x = v ∧ y = u) → (∃z∃wφ ↔ ∃z∃wψ))
3	2	cbvex2v 976	. 2 ⊢ (∃x∃y∃z∃wφ ↔ ∃v∃u∃z∃wψ)
4		cbvex4v.2	. . . 4 ⊢ ((z = f ∧ w = g) → (ψ ↔ χ))
5	4	cbvex2v 976	. . 3 ⊢ (∃z∃wψ ↔ ∃f∃gχ)
6	5	bi2ex 734	. 2 ⊢ (∃v∃u∃z∃wψ ↔ ∃v∃u∃f∃gχ)
7	3, 6	bitr 151	1 ⊢ (∃x∃y∃z∃wφ ↔ ∃v∃u∃f∃gχ)

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196  ∃wex 678   = weq 797

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-12 802  ax-17 925

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679

metamath.org