Theorem vtoclbg 1384

Description: Implicit substitution of a class for a set variable.

Hypotheses

Ref	Expression
vtoclbg.1	⊢ (x = A → (φ ↔ χ))
vtoclbg.2	⊢ (x = A → (ψ ↔ θ))
vtoclbg.3	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
vtoclbg	⊢ (A ∈ B → (χ ↔ θ))

Distinct variable group(s):   x,A   χ,x   θ,x

Proof of Theorem vtoclbg

Step	Hyp	Ref	Expression
1		vtoclbg.1	. . 3 ⊢ (x = A → (φ ↔ χ))
2		vtoclbg.2	. . 3 ⊢ (x = A → (ψ ↔ θ))
3	1, 2	bibi12d 477	. 2 ⊢ (x = A → ((φ ↔ ψ) ↔ (χ ↔ θ)))
4		vtoclbg.3	. 2 ⊢ (φ ↔ ψ)
5	3, 4	vtoclg 1383	1 ⊢ (A ∈ B → (χ ↔ θ))

Syntax hints:   → wi 2   ↔ wb 127   = wceq 1091   ∈ wcel 1092

This theorem is referenced by:  eqvinc 1407  sbcco 1448  sbcn 1459  sbcim 1460  sbcan 1461  sbcor 1462  sbcbi 1463  sbcal 1464  sbcex 1465  snssg 1850  opthg 1899  elopab 2110  elomg 2376  opelxp 2452  opelxpg 2454  eldmg 2529  ndmfv 2848  funfvima3 2906

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  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349

metamath.org