Theorem vtoclbg 3536

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-clel 2809

This theorem is referenced by:  alexeqg  3630  pm13.183  3645  elab6g  3648  elabgw  3656  sbc8g  3773  sbc2or  3774  sbccow  3788  sbcco  3791  sbc5ALT  3794  sbcie2g  3806  eqsbc1  3812  sbcng  3813  sbcimg  3814  sbcan  3815  sbcor  3816  sbcbig  3817  sbcal  3825  sbcex2  3826  sbcel1v  3831  sbcreu  3851  csbiebg  3906  sbcel12  4386  sbceqg  4387  csbie2df  4418  preq12bg  4829  elintrabg  4937  sbcbr123  5173  inisegn0  6085  fsn2g  7128  funfvima3  7228  elixpsn  8951  ixpsnf1o  8952  domeng  8977  1sdomOLD  9257  rankcf  10791  eldm3  35778  elima4  35793  brsset  35907  brbigcup  35916  elfix2  35922  elfunsg  35934  elsingles  35936  funpartlem  35960  ellines  36170  elhf2g  36194  bj-elpwgALT  37072  cover2g  37740  sbcrexgOLD  42808