Theorem vtoclbg 3472

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-clel 2811

This theorem is referenced by:  alexeqg  3547  pm13.183  3564  elab6g  3570  sbc8g  3688  sbc2or  3689  sbccow  3703  sbcco  3706  sbc5ALT  3709  sbcie2g  3721  eqsbc3  3727  sbcng  3728  sbcimg  3729  sbcan  3730  sbcor  3731  sbcbig  3732  sbcal  3742  sbcex2  3743  sbcel1v  3748  sbcreu  3767  csbiebg  3822  sbcel12  4298  sbceqg  4299  csbie2df  4330  elpwgOLD  4495  preq12bg  4739  elintrabg  4849  sbcbr123  5084  inisegn0  5935  fsn2g  6910  funfvima3  7009  elixpsn  8547  ixpsnf1o  8548  domeng  8569  1sdom  8800  rankcf  10277  eldm3  33300  elima4  33322  brsset  33829  brbigcup  33838  elfix2  33844  elfunsg  33856  elsingles  33858  funpartlem  33882  ellines  34092  elhf2g  34116  cover2g  35496  elabgw  39756  sbcrexgOLD  40179