Theorem vtoclbg 3517

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 349	. 2 ⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ 𝜃)))
4		vtoclbg.3	. 2 ⊢ (𝜑 ↔ 𝜓)
5	3, 4	vtoclg 3515	1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∈ wcel 2111

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870

This theorem is referenced by:  alexeqg  3592  pm13.183  3606  elabgw  3612  sbc8g  3728  sbc2or  3729  sbccow  3743  sbcco  3746  sbc5  3748  sbcie2g  3759  eqsbc3  3765  sbcng  3766  sbcimg  3767  sbcan  3768  sbcor  3769  sbcbig  3770  sbcal  3780  sbcex2  3781  sbcel1v  3786  sbcreu  3805  csbiebg  3860  sbcel12  4316  sbceqg  4317  csbie2df  4348  elpwgOLD  4504  preq12bg  4744  elintrabg  4851  sbcbr123  5084  inisegn0  5928  fsn2g  6877  funfvima3  6976  elixpsn  8484  ixpsnf1o  8485  domeng  8506  1sdom  8705  rankcf  10188  eldm3  33110  elima4  33132  brsset  33463  brbigcup  33472  elfix2  33478  elfunsg  33490  elsingles  33492  funpartlem  33516  ellines  33726  elhf2g  33750  cover2g  35153  sbcrexgOLD  39726