Theorem vtoclbg 3503

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 3500	1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-clel 2812

This theorem is referenced by:  alexeqg  3594  pm13.183  3609  elab6g  3612  elabgw  3621  sbc8g  3737  sbc2or  3738  sbccow  3752  sbcco  3755  sbc5ALT  3758  sbcie2g  3770  eqsbc1  3776  sbcng  3777  sbcimg  3778  sbcan  3779  sbcor  3780  sbcbig  3781  sbcal  3789  sbcex2  3790  sbcel1v  3795  sbcreu  3815  csbiebg  3870  sbcel12  4352  sbceqg  4353  csbie2df  4384  preq12bg  4797  elintrabg  4904  sbcbr123  5140  inisegn0  6058  fsn2g  7086  funfvima3  7185  elixpsn  8879  ixpsnf1o  8880  domeng  8903  rankcf  10694  eldm3  35962  elima4  35977  brsset  36088  brbigcup  36097  elfix2  36103  elfunsg  36115  elsingles  36117  funpartlem  36143  ellines  36353  elhf2g  36377  bj-elpwgALT  37380  cover2g  38054  sbcrexgOLD  43234