Theorem vtoclbg 3568

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533   ∈ wcel 2110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-nf 1781  df-cleq 2814  df-clel 2893

This theorem is referenced by:  alexeqg  3643  pm13.183  3658  pm13.183OLD  3659  sbc8g  3779  sbc2or  3780  sbccow  3794  sbcco  3797  sbc5  3799  sbcie2g  3810  eqsbc3  3816  eqsbc3OLD  3817  sbcng  3818  sbcimg  3819  sbcan  3820  sbcor  3821  sbcbig  3822  sbcal  3832  sbcex2  3833  sbcel1v  3838  sbcel1vOLD  3839  sbcreu  3858  csbiebg  3914  sbcel12  4359  sbceqg  4360  csbie2df  4391  elpwgOLD  4545  preq12bg  4783  elintrabg  4888  sbcbr123  5119  inisegn0  5960  fsn2g  6899  funfvima3  6997  elixpsn  8500  ixpsnf1o  8501  domeng  8522  1sdom  8720  rankcf  10198  eldm3  32997  elima4  33019  brsset  33350  brbigcup  33359  elfix2  33365  elfunsg  33377  elsingles  33379  funpartlem  33403  ellines  33613  elhf2g  33637  cover2g  34989  sbcrexgOLD  39380