Theorem vtoclbg 3524

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-clel 2838

This theorem is referenced by:  alexeqg  3610  pm13.183  3625  elab6g  3628  elabgw  3636  sbc8g  3752  sbc2or  3753  sbccow  3767  sbcco  3770  sbc5ALT  3773  sbcie2g  3784  eqsbc1  3790  sbcng  3791  sbcimg  3792  sbcan  3793  sbcor  3794  sbcbig  3795  sbcal  3803  sbcex2  3804  sbcel1v  3809  sbcreu  3829  csbiebg  3885  sbcel12  4376  sbceqg  4377  csbie2df  4408  preq12bg  4818  elintrabg  4926  sbcbr123  5165  inisegn0  6100  fsn2g  7134  funfvima3  7234  elixpsn  8931  ixpsnf1o  8932  domeng  8955  rankcf  10757  kardeng  35570  eldm3  36253  elima4  36268  brsset  36379  brbigcup  36388  elfix2  36394  elfunsg  36406  elsingles  36408  funpartlem  36434  ellines  36644  elhf2g  36668  bj-elpwgALT  37710  cover2g  38387