Theorem vtoclbg 3505

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

Hypotheses

Ref	Expression
vtoclbg.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
vtoclbg.2	⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
vtoclbg.3	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
vtoclbg	⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Distinct variable groups:   𝑥,𝐴   𝜒,𝑥   𝜃,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝑉(𝑥)

Proof of Theorem vtoclbg

Step	Hyp	Ref	Expression
1		vtoclbg.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
2		vtoclbg.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
3	1, 2	bibi12d 345	. 2 ⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ 𝜃)))
4		vtoclbg.3	. 2 ⊢ (𝜑 ↔ 𝜓)
5	3, 4	vtoclg 3503	1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-clel 2817

This theorem is referenced by:  alexeqg  3581  pm13.183  3598  elab6g  3601  sbc8g  3727  sbc2or  3728  sbccow  3742  sbcco  3745  sbc5ALT  3748  sbcie2g  3761  eqsbc1  3768  sbcng  3769  sbcimg  3770  sbcan  3771  sbcor  3772  sbcbig  3773  sbcal  3784  sbcex2  3785  sbcel1v  3791  sbcreu  3813  csbiebg  3869  sbcel12  4347  sbceqg  4348  csbie2df  4379  elpwgOLD  4545  preq12bg  4789  elintrabg  4897  sbcbr123  5132  inisegn0  6003  fsn2g  7004  funfvima3  7106  elixpsn  8699  ixpsnf1o  8700  domeng  8723  1sdom  8987  rankcf  10517  eldm3  33707  elima4  33729  brsset  34170  brbigcup  34179  elfix2  34185  elfunsg  34197  elsingles  34199  funpartlem  34223  ellines  34433  elhf2g  34457  cover2g  35852  elabgw  40145  sbcrexgOLD  40587