Theorem vtoclbg 3512

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-clel 2809

This theorem is referenced by:  alexeqg  3603  pm13.183  3618  elab6g  3621  elabgw  3630  sbc8g  3746  sbc2or  3747  sbccow  3761  sbcco  3764  sbc5ALT  3767  sbcie2g  3779  eqsbc1  3785  sbcng  3786  sbcimg  3787  sbcan  3788  sbcor  3789  sbcbig  3790  sbcal  3798  sbcex2  3799  sbcel1v  3804  sbcreu  3824  csbiebg  3879  sbcel12  4361  sbceqg  4362  csbie2df  4393  preq12bg  4807  elintrabg  4914  sbcbr123  5150  inisegn0  6055  fsn2g  7081  funfvima3  7180  elixpsn  8873  ixpsnf1o  8874  domeng  8897  rankcf  10686  eldm3  35904  elima4  35919  brsset  36030  brbigcup  36039  elfix2  36045  elfunsg  36057  elsingles  36059  funpartlem  36085  ellines  36295  elhf2g  36319  bj-elpwgALT  37198  cover2g  37856  sbcrexgOLD  42969