Theorem vtoclbg 2915

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.)

Hypotheses

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

Assertion

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

Distinct variable groups:   x,A   χ,x   θ,x

Allowed substitution hints:   φ(x)   ψ(x)   V(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 312	. 2 ⊢ (x = A → ((φ ↔ ψ) ↔ (χ ↔ θ)))
4		vtoclbg.3	. 2 ⊢ (φ ↔ ψ)
5	3, 4	vtoclg 2914	1 ⊢ (A ∈ V → (χ ↔ θ))

Syntax hints:   → wi 4   ↔ wb 176   = wceq 1642   ∈ wcel 1710

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-v 2861

This theorem is referenced by:  pm13.183  2979  sbc8g  3053  sbc2or  3054  sbcco  3068  sbc5  3070  sbcie2g  3079  eqsbc3  3085  sbcng  3086  sbcimg  3087  sbcan  3088  sbcang  3089  sbcor  3090  sbcorg  3091  sbcbig  3092  sbcal  3093  sbcalg  3094  sbcex2  3095  sbcexg  3096  sbc3ang  3104  sbcel1gv  3105  sbcel2gv  3106  sbcralg  3120  sbcrexg  3121  sbcreug  3122  sbcel12g  3151  sbceqg  3152  csbiebg  3175  elpwg  3729  snssg  3844  elintg  3934  elintrabg  3939  preq12bg  4128  sbcbrg  4685  opbr1st  5501  opbr2nd  5502  elfix  5787  otelins2  5791  otelins3  5792  elfunsg  5830  brfns  5833