Theorem vtoclbg 3516

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-clel 2812

This theorem is referenced by:  alexeqg  3607  pm13.183  3622  elab6g  3625  elabgw  3634  sbc8g  3750  sbc2or  3751  sbccow  3765  sbcco  3768  sbc5ALT  3771  sbcie2g  3783  eqsbc1  3789  sbcng  3790  sbcimg  3791  sbcan  3792  sbcor  3793  sbcbig  3794  sbcal  3802  sbcex2  3803  sbcel1v  3808  sbcreu  3828  csbiebg  3883  sbcel12  4365  sbceqg  4366  csbie2df  4397  preq12bg  4811  elintrabg  4918  sbcbr123  5154  inisegn0  6065  fsn2g  7093  funfvima3  7192  elixpsn  8887  ixpsnf1o  8888  domeng  8911  rankcf  10700  eldm3  35977  elima4  35992  brsset  36103  brbigcup  36112  elfix2  36118  elfunsg  36130  elsingles  36132  funpartlem  36158  ellines  36368  elhf2g  36392  bj-elpwgALT  37302  cover2g  37967  sbcrexgOLD  43142